Papers with proof-relevant program components
Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis (2026.acl-demo)
Copied to clipboard
Cheng Wen, Hu Junjie, YiKun Hu, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun, Shengchao Qin, Cong Tian
| Challenge: | Formal verification typically requires developers to write detailed formal specifications . a formal verification system that generates candidate specifications is costly and error-prone . |
| Approach: | They propose an LLM-driven neuro-symbolic demonstration system that reframes specification writing as constrained structured synthesis. |
| Outcome: | The proposed system reduces hallucinations and produces proof-ready annotations. |